Nuprl Lemma : firstn_all
0,22
postcript
pdf
L
:Top List,
n
:
. ||
L
||
n
(firstn(
n
;
L
) ~
L
)
latex
Definitions
i
j
,
Unit
,
P
Q
,
P
&
Q
,
P
Q
,
T
,
i
<
j
,
,
i
j
,
b
,
b
,
True
,
Prop
,
A
,
False
,
P
Q
,
firstn(
n
;
as
)
,
A
B
,
||
as
||
,
x
:
A
.
B
(
x
)
,
Top
,
t
T
Lemmas
top
wf
,
length
wf1
,
le
wf
,
bnot
wf
,
assert
wf
,
le
int
wf
,
bool
wf
,
lt
int
wf
,
assert
of
le
int
,
bnot
of
lt
int
,
true
wf
,
squash
wf
,
eqff
to
assert
,
iff
transitivity
,
assert
of
lt
int
,
eqtt
to
assert
,
non
neg
length
origin